ds:x:Id fp Type, da:k:Knd fp Type, x:Id, T:Type, ks:Knd List,
a:((k:{k:Knd| (k  ks) }State(ds)Valtype(da;k)T)), snd:msg-spec(ds;da).
x  dom(ds)  ecl-machine3(ds;da;x;T;ks;a;snd)  Realizer 

latex

Definitions	Id, t  T, Type, x. t(x), x:A. B(x), a:A fp B(a), Knd, type List, , x:AB(x), Valtype(da;k), State(ds), (x  l), {x:A| B(x) }, , msg-spec(ds;da), x.A(x), Top, IdDeq, x  dom(f), b, A, msg-spec-links(snd), IdLnkDeq, IdLnk, remove-repeats(eq;L), P  Q, ecl-m3(a;snd;x;l), ecl-tags(l;snd), x : v, f  g, R-lnk-tags(ds;da;l;tgs;ks;g), xL.R(x), ecl-machine3(ds;da;x;T;ks;a;snd)
Lemmas	Rall wf, R-lnk-tags wf, fpf-join wf, fpf-single wf, ecl-tags wf, ecl-m3 wf, remove-repeats wf, IdLnk wf, idlnk-deq wf, msg-spec-links wf, not wf, assert wf, fpf-dom wf, id-deq wf, fpf-trivial-subtype-top, msg-spec wf, nat wf, l member wf, decl-state wf, ma-valtype wf, bool wf, Knd wf, fpf wf, Id wf